Nuprl Lemma : nequal_wf 12,41

A:Type, xy:Ax  y  A    
latex


ProofTree


Definitionsa  b  T , , t  T, x:AB(x)
Lemmasnot wf

origin